\begin{tabbing}
R{-}state{-}var($i$; ${\it ds}$; ${\it da}$; $x$; $T$; ${\it ks}$; ${\it tr}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$Rplus(\=Rall(\=${\it ks}$;\+\+
\\[0ex]$k$.Reffect(\=$i$;\+
\\[0ex]fpf{-}join(id{-}deq; ${\it ds}$; fpf{-}single($x$; $T$));
\\[0ex]$k$;
\\[0ex]ma{-}valtype(${\it da}$; $k$);
\\[0ex]$x$;
\\[0ex](inl ($\lambda$$s$,$v$. ${\it tr}$($k$,$s$,$v$,$s$($x$))) )));
\-\-\\[0ex]Rframe($i$; $T$; $x$; ${\it ks}$))
\-
\end{tabbing}